SherbyNet - /page/wikibook/entry.mu

<!DOCTYPE html>

<title>SLD resolution</title>

</head>

<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">SLD resolution</span></span>

</h1>

</header>

<p><b>SLD resolution</b> (<i>Selective Linear Definite</i> clause resolution) is the basic <a href="Rule_of_inference" title="Rule of inference">inference rule</a> used in <a href="Logic_programming" title="Logic programming">logic programming</a>. It is a refinement of <a href="Resolution_(logic)" title="Resolution (logic)">resolution</a>, which is both <a href="Soundness" title="Soundness">sound</a> and refutation <a href="Completeness_(logic)" title="Completeness (logic)">complete</a> for <a href="Horn_clause" title="Horn clause">Horn clauses</a>.

</p>

<div class="mw-heading mw-heading2"><h2 id="The_SLD_inference_rule">The SLD inference rule</h2></div>

<p>Given a goal clause, represented as the negation of a problem to be solved:

</p><p><span class="mwe-math-element mwe-math-element-block"><span class="mwe-math-mathml-display mwe-math-mathml-a11y" style="display: none;"><math display="block" xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}}</annotation>

</semantics>

</math></span></span>

</p><p>with selected literal <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg L_{i}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg L_{i}}</annotation>

</semantics>

</math></span><img src="./61a67c32bb6bec92ee922be34766544f463d2f34.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.933ex; height:2.509ex;" alt="{\displaystyle \neg L_{i}}" loading="lazy"></span>, and an input <a href="Definite_clause" class="mw-redirect" title="Definite clause">definite clause</a>:

</p><p><span class="mwe-math-element mwe-math-element-block"><span class="mwe-math-mathml-display mwe-math-mathml-a11y" style="display: none;"><math display="block" xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L\lor \neg K_{1}\lor \cdots \lor \neg K_{m}}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle L\lor \neg K_{1}\lor \cdots \lor \neg K_{m}}</annotation>

</semantics>

</math></span></span>

</p><p>whose positive literal (atom) <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L\,}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle L\,}</annotation>

</semantics>

</math></span><img src="./d330bc0cd693cc87e3943137dc591038a89f77e2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.97ex; height:2.176ex;" alt="{\displaystyle L\,}" loading="lazy"></span> <a href="Unification_(computing)" class="mw-redirect" title="Unification (computing)">unifies</a> with the atom <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{i}\,}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle L_{i}\,}</annotation>

</semantics>

</math></span><img src="./0d382c1455269cfb6ee37f3265954c3326b3f60b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.77ex; height:2.509ex;" alt="{\displaystyle L_{i}\,}" loading="lazy"></span> of the selected literal <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg L_{i}\,}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg L_{i}\,}</annotation>

</semantics>

</math></span><img src="./5d35648d963d480903984324a775557095e6ccbd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.32ex; height:2.509ex;" alt="{\displaystyle \neg L_{i}\,}" loading="lazy"></span>, SLD resolution derives another goal clause, in which the selected literal is replaced by the negative literals of the input clause and the unifying substitution <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \theta \,}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \theta \,}</annotation>

</semantics>

</math></span><img src="./228647b7d4a18b6c8c0c390b439a61da8fafec76.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.478ex; height:2.176ex;" alt="{\displaystyle \theta \,}" loading="lazy"></span> is applied:

</p><p><span class="mwe-math-element mwe-math-element-block"><span class="mwe-math-mathml-display mwe-math-mathml-a11y" style="display: none;"><math display="block" xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (\neg L_{1}\lor \cdots \lor \neg K_{1}\lor \cdots \lor \neg K_{m}\ \lor \cdots \lor \neg L_{n})\theta }">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (\neg L_{1}\lor \cdots \lor \neg K_{1}\lor \cdots \lor \neg K_{m}\ \lor \cdots \lor \neg L_{n})\theta }</annotation>

</semantics>

</math></span></span>

</p><p>In the simplest case, in propositional logic, the atoms <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{i}\,}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle L_{i}\,}</annotation>

</semantics>

</math></span><img src="./0d382c1455269cfb6ee37f3265954c3326b3f60b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.77ex; height:2.509ex;" alt="{\displaystyle L_{i}\,}" loading="lazy"></span> and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L\,}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle L\,}</annotation>

</semantics>

</math></span><img src="./d330bc0cd693cc87e3943137dc591038a89f77e2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.97ex; height:2.176ex;" alt="{\displaystyle L\,}" loading="lazy"></span> are identical, and the unifying substitution <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \theta \,}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \theta \,}</annotation>

</semantics>

</math></span><img src="./228647b7d4a18b6c8c0c390b439a61da8fafec76.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.478ex; height:2.176ex;" alt="{\displaystyle \theta \,}" loading="lazy"></span> is vacuous. However, in the more general case, the unifying substitution is necessary to make the two literals identical.

</p>

<div class="mw-heading mw-heading2"><h2 id="The_origin_of_the_name_"SLD"">The origin of the name "SLD"</h2></div>

<p>The name "SLD resolution" was given by Maarten van Emden for the unnamed inference rule introduced by <a href="Robert_Kowalski" title="Robert Kowalski">Robert Kowalski</a>.<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> Its name is derived from SL resolution,<sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> which is both sound and refutation complete for the unrestricted clausal form of logic. "SLD" stands for "SL resolution with Definite clauses".

</p><p>In both, SL and SLD, "L" stands for the fact that a resolution proof can be restricted to a linear sequence of clauses:

</p><p><span class="mwe-math-element mwe-math-element-block"><span class="mwe-math-mathml-display mwe-math-mathml-a11y" style="display: none;"><math display="block" xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1},C_{2},\cdots ,C_{l}}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{1},C_{2},\cdots ,C_{l}}</annotation>

</semantics>

</math></span></span>

</p><p>where the "top clause" <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1}\,}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{1}\,}</annotation>

</semantics>

</math></span><img src="./d3d4f3c02d474547c70098d2529c8636829776a3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.103ex; height:2.509ex;" alt="{\displaystyle C_{1}\,}" loading="lazy"></span> is an input clause, and every other clause <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{i+1}\,}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{i+1}\,}</annotation>

</semantics>

</math></span><img src="./741a11990e8b167d6821f56baaf34e09eba10ac5.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.949ex; height:2.509ex;" alt="{\displaystyle C_{i+1}\,}" loading="lazy"></span> is a resolvent one of whose parents is the previous clause <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{i}\,}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{i}\,}</annotation>

</semantics>

</math></span><img src="./f72b1de783f93ff6f0d055e04a91519368ab9310.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.849ex; height:2.509ex;" alt="{\displaystyle C_{i}\,}" loading="lazy"></span>. The proof is a refutation if the last clause <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{l}\,}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{l}\,}</annotation>

</semantics>

</math></span><img src="./f2156736f1ad69c9b903212ace4fbcd08bde87c7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.771ex; height:2.509ex;" alt="{\displaystyle C_{l}\,}" loading="lazy"></span> is the empty clause.

</p><p>In SLD, all of the clauses in the sequence are goal clauses, and the other parent is an input clause. In SL resolution, the other parent is either an input clause or an ancestor clause earlier in the sequence.

</p><p>In both SL and SLD, "S" stands for the fact that the only literal resolved upon in any clause <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{i}\,}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{i}\,}</annotation>

</semantics>

</math></span><img src="./f72b1de783f93ff6f0d055e04a91519368ab9310.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.849ex; height:2.509ex;" alt="{\displaystyle C_{i}\,}" loading="lazy"></span> is one that is uniquely selected by a selection rule or selection function. In SL resolution, the selected literal is restricted to one which has been most recently introduced into the clause. In the simplest case, such a <a href="Stack_(abstract_data_type)" title="Stack (abstract data type)">last-in-first-out</a> selection function can be specified by the order in which literals are written, as in <a href="Prolog" title="Prolog">Prolog</a>. However, the selection function in SLD resolution is more general than in SL resolution and in Prolog. There is no restriction on the literal that can be selected.

</p>

<div class="mw-heading mw-heading2"><h2 id="The_computational_interpretation_of_SLD_resolution">The computational interpretation of SLD resolution</h2></div>

<p>In clausal logic, an SLD refutation demonstrates that the input set of clauses is unsatisfiable. In logic programming, however, an SLD refutation also has a computational interpretation. The top clause <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}}</annotation>

</semantics>

</math></span><img src="./5f44ac5d0a865f6d3babee1a9e58aaf6f4ae96ef.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:28.249ex; height:2.509ex;" alt="{\displaystyle \neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}}" loading="lazy"></span> can be interpreted as the denial of a conjunction of subgoals <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1}\land \cdots \land L_{i}\land \cdots \land L_{n}}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle L_{1}\land \cdots \land L_{i}\land \cdots \land L_{n}}</annotation>

</semantics>

</math></span><img src="./e518a1160ad51d9b232ed8de9190b18a93858e7b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:23.598ex; height:2.509ex;" alt="{\displaystyle L_{1}\land \cdots \land L_{i}\land \cdots \land L_{n}}" loading="lazy"></span>. The derivation of clause <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{i+1}\,}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{i+1}\,}</annotation>

</semantics>

</math></span><img src="./741a11990e8b167d6821f56baaf34e09eba10ac5.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.949ex; height:2.509ex;" alt="{\displaystyle C_{i+1}\,}" loading="lazy"></span> from <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{i}\,}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{i}\,}</annotation>

</semantics>

</math></span><img src="./f72b1de783f93ff6f0d055e04a91519368ab9310.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.849ex; height:2.509ex;" alt="{\displaystyle C_{i}\,}" loading="lazy"></span> is the derivation, by means of <a href="Backward_reasoning" class="mw-redirect" title="Backward reasoning">backward reasoning</a>, of a new set of sub-goals using an input clause as a goal-reduction procedure. The unifying substitution <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \theta \,}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \theta \,}</annotation>

</semantics>

</math></span><img src="./228647b7d4a18b6c8c0c390b439a61da8fafec76.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.478ex; height:2.176ex;" alt="{\displaystyle \theta \,}" loading="lazy"></span> both passes input from the selected subgoal to the body of the procedure and simultaneously passes output from the head of the procedure to the remaining unselected subgoals. The empty clause is simply an empty set of subgoals, which signals that the initial conjunction of subgoals in the top clause has been solved.

</p>

<div class="mw-heading mw-heading2"><h2 id="SLD_resolution_strategies">SLD resolution strategies</h2></div>

<p>SLD resolution implicitly defines a <a href="Search_tree" title="Search tree">search tree</a> of alternative computations, in which the initial goal clause is associated with the root of the tree. For every node in the tree and for every definite clause in the program whose positive literal unifies with the selected literal in the goal clause associated with the node, there is a child node associated with the goal clause obtained by SLD resolution.

</p><p>A leaf node, which has no children, is a success node if its associated goal clause is the empty clause. It is a failure node if its associated goal clause is non-empty but its selected literal unifies with no positive literal of definite clauses in the program.

</p><p>SLD resolution is non-deterministic in the sense that it does not determine the search strategy for exploring the search tree. Prolog searches the tree depth-first, one branch at a time, using backtracking when it encounters a failure node. <a href="Depth-first_search" title="Depth-first search">Depth-first search</a> is very efficient in its use of computing resources, but is incomplete if the search space contains infinite branches and the search strategy searches these in preference to finite branches: the computation does not terminate. Other search strategies, including <a href="Breadth-first_search" title="Breadth-first search">breadth-first</a>, <a href="Best-first_search" title="Best-first search">best-first</a>, and <a href="Branch-and-bound" class="mw-redirect" title="Branch-and-bound">branch-and-bound</a> search are also possible. Moreover, the search can be carried out sequentially, one node at a time, or in parallel, many nodes simultaneously.

</p><p>SLD resolution is also non-deterministic in the sense, mentioned earlier, that the selection rule is not determined by the inference rule, but is determined by a separate decision procedure, which can be sensitive to the dynamics of the program execution process.

</p><p>The SLD resolution search space is an or-tree, in which different branches represent alternative computations. In the case of propositional logic programs, SLD can be generalised so that the search space is an <a href="And-or_tree" class="mw-redirect" title="And-or tree">and-or tree</a>, whose nodes are labelled by single literals, representing subgoals, and nodes are joined either by conjunction or by disjunction. In the general case, where conjoint subgoals share variables, the and-or tree representation is more complicated.

</p>

<div class="mw-heading mw-heading2"><h2 id="Example">Example</h2></div>

<p>Given the logic program in the <a href="Prolog" title="Prolog">Prolog</a> language:

</p>

</pre></div>

<p>and the top-level goal:

</p>

</pre></div>

<p>the search space consists of a single branch, in which <code>q</code> is reduced to <code>p</code> which is reduced to the empty set of subgoals, signalling a successful computation. In this case, the program is so simple that there is no role for the selection function and no need for any search.

</p><p>In clausal logic, the program is represented by the set of clauses:

</p><p><span class="mwe-math-element mwe-math-element-block"><span class="mwe-math-mathml-display mwe-math-mathml-a11y" style="display: none;"><math display="block" xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle q\lor \neg p}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle q\lor \neg p}</annotation>

</semantics>

</math></span></span>

</p><p><span class="mwe-math-element mwe-math-element-block"><span class="mwe-math-mathml-display mwe-math-mathml-a11y" style="display: none;"><math display="block" xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p\,}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p\,}</annotation>

</semantics>

</math></span></span>

</p><p>and top-level goal is represented by the goal clause with a single negative literal:

</p><p><span class="mwe-math-element mwe-math-element-block"><span class="mwe-math-mathml-display mwe-math-mathml-a11y" style="display: none;"><math display="block" xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg q}</annotation>

</semantics>

</math></span></span>

</p><p>The search space consists of the single refutation:

</p><p><span class="mwe-math-element mwe-math-element-block"><span class="mwe-math-mathml-display mwe-math-mathml-a11y" style="display: none;"><math display="block" xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg q,\neg p,{\mathit {false}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg q,\neg p,{\mathit {false}}}</annotation>

</semantics>

</math></span></span>

</p><p>where <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathit {false}}\,}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathit {false}}\,}</annotation>

</semantics>

</math></span><img src="./8a28ce6d2b3d13504e9b9ba05a60e1b1df1f1d84.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.052ex; width:4.958ex; height:2.509ex;" alt="{\displaystyle {\mathit {false}}\,}" loading="lazy"></span> represents the empty clause.

</p><p>If the following clause were added to the program:

</p>

</pre></div>

<p>then there would be an additional branch in the search space, whose leaf node <code>r</code> is a failure node. In Prolog, if this clause were added to the front of the original program, then Prolog would use the order in which the clauses are written to determine the order in which the branches of the search space are investigated. Prolog would try this new branch first, fail, and then backtrack to investigate the single branch of the original program and succeed.

</p><p>If the clause

</p>

</pre></div>

<p>were now added to the program, then the search tree would contain an infinite branch. If this clause were tried first, then Prolog would go into an infinite loop and not find the successful branch.

</p>

<div class="mw-heading mw-heading2"><h2 id="SLDNF">SLDNF</h2></div>

<p>SLDNF<sup id="cite_ref-3" class="reference"><a href="#cite_note-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup> is an extension of SLD resolution to deal with <a href="Negation_as_failure" title="Negation as failure">negation as failure</a>. In SLDNF, goal clauses can contain negation as failure literals, say of the form <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle not(p)\,}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle not(p)\,}</annotation>

</semantics>

</math></span><img src="./a495dbd34112493ba36e58b4f8357d49ed0515e6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.728ex; height:2.843ex;" alt="{\displaystyle not(p)\,}" loading="lazy"></span>, which can be selected only if they contain no variables. When such a variable-free literal is selected, a subproof (or subcomputation) is attempted to determine whether there is an SLDNF refutation starting from the corresponding unnegated literal <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p\,}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p\,}</annotation>

</semantics>

</math></span><img src="./e4fa5f88a712eb9b03398066a0577fdcf33e02c6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:1.646ex; height:2.009ex;" alt="{\displaystyle p\,}" loading="lazy"></span> as top clause. The selected subgoal <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle not(p)\,}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle not(p)\,}</annotation>

</semantics>

</math></span><img src="./a495dbd34112493ba36e58b4f8357d49ed0515e6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.728ex; height:2.843ex;" alt="{\displaystyle not(p)\,}" loading="lazy"></span> succeeds if the subproof fails, and it fails if the subproof succeeds.

</p>

<ul><li><a href="John_Alan_Robinson" title="John Alan Robinson">John Alan Robinson</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

<li id="cite_note-1"><span class="mw-cite-backlink"><b><a href="#cite_ref-1">^</a></b></span> <span class="reference-text">Robert Kowalski <a rel="nofollow" class="external text" href="http://www.doc.ic.ac.uk/~rak/papers/IFIP%2074.pdf">Predicate Logic as a Programming Language</a> Memo 70, Department of Artificial Intelligence, University of Edinburgh. 1973. Also in Proceedings IFIP Congress, Stockholm, North Holland Publishing Co., 1974, pp. 569-574.</span>

</li>

<li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text">Robert Kowalski and Donald Kuehner, <a rel="nofollow" class="external text" href="http://www.doc.ic.ac.uk/~rak/papers/sl.pdf">Linear Resolution with Selection Function</a> <a href="Artificial_Intelligence_(journal)" title="Artificial Intelligence (journal)">Artificial Intelligence</a>, Vol. 2, 1971, pp. 227-60.</span>

</li>

<li id="cite_note-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-3">^</a></b></span> <span class="reference-text"><a href="Krzysztof_R._Apt" title="Krzysztof R. Apt">Krzysztof Apt</a> and Maarten van Emden, <a rel="nofollow" class="external text" href="http://dl.acm.org/citation.cfm?doid=322326.322339">Contributions to the Theory of Logic Programming</a>, <a href="Journal_of_the_Association_for_Computing_Machinery" class="mw-redirect" title="Journal of the Association for Computing Machinery">Journal of the Association for Computing Machinery</a>. Vol, 1982 - portal.acm.org</span>

</li>

</ol></div>

<ul><li><a href="Jean_Gallier" title="Jean Gallier">Jean Gallier</a>, <i><a rel="nofollow" class="external text" href="https://cs.uwaterloo.ca/~david/cl/sld-gallier.pdf">SLD-Resolution and Logic Programming</a></i> chapter 9 of <i><a rel="nofollow" class="external text" href="http://www.cis.upenn.edu/~jean/gbooks/logic.html">Logic for Computer Science: Foundations of Automatic Theorem Proving</a></i>, 2003 online revision (free to download), originally published by Wiley, 1986</li>

<li>John C. Shepherdson, <i>SLDNF-Resolution with Equality</i>, <a href="Journal_of_Automated_Reasoning" title="Journal of Automated Reasoning">Journal of Automated Reasoning</a> 8: 297-306, 1992; defines semantics with respect to which SLDNF-resolution with equality is sound and complete</li></ul>

<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>

<ul><li><a rel="nofollow" class="external autonumber" href="http://foldoc.org/?SLD+resolution">[1]</a> Definition from the Free On-Line Dictionary of Computing</li></ul></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-04-30" href="https://en.wikipedia.org/wiki/?title=SLD_resolution&oldid=1288133584">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>